es, C, T, S, R, codes, decodes, Req, Ack:Top.
for clients C sends FIFO
forfrom j to i via (S[j,i],codes)
forreceives at i via (R[i],decodes) requests Req[j] are acknowledged by Ack[j,i]
~
(
i:C.
f:{e:E| R(i,e)} 
{e:E| j:C. (S(j,i,e))}
fifo+property(es;codes;decodes;C;S;R;T;Req;Ack;i;f)) 
T